| Definitions |  x:A. B(x), Id, P   Q, x L. P(x), P & Q, "$x", ecl-machine at i with state $eclAstate variables dsactions dasends sndupdates upd,  , ecl-trans-ks(v), t T, let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), Normal(T), Prop,  T, True, SQType(T), {T},   x. t(x), R ||- es.P(es), R-Feasible(R), ecl-trans-type(A), ecl-trans-a(v), 1of(t), S  T, S  T, @i[[x;snd;upd]], @i[[x;snd]], if b t else f fi, true, false, State(ds), state@i, Valtype(da;k), P  Q, 2of(t), tagged-list-messages(s;v;L), ecl-m3(a;snd;x;l), mapfilter(f;P;L), let x = a in b(x), map(f;as), let x,y,z = a in t(x;y;z), filter(P;l), concat(ll), Y, reduce(f;k;as), as @ bs, Top, A & B, x when e, s.x,  A, x(s), e@i. P(e), f(x)?z, @i[[x;upd]], es-trans-state-from{i:l}(es;ks;g;z;e1;e2), list_accum(x,a.f(x;a);y;l), es-hist{i:l}(es;e1;e2), es-info(es;e), x,y. t(x;y), (state when e), P  Q, P Q, ecl-trans-tuple{i:l}(ds;da), ||as||, Consistent(R;es), msg-spec-loc(snd;i),  , Unit, msg-spec(ds;da), msg-item(ds;da;k;l), False, update-spec-decl(upd;ds), e' e.P(e'), update-spec(ds;da), (x l), x(s1,s2),  x:A. B(x),  |
| Lemmas | ecl-machine1-realizes, ecl-kinds-ecl-trans, atom-free-ecl-trans-type, ecl-trans wf, ecl-trans-tuple wf, ecl-machine2-realizes, l member wf, squash wf, true wf, Knd sq, length wf1, non neg length, le wf, cons one one, ecl-trans-ks wf, ecl-machine3-realizes, atom-free wf, ecl-trans-type wf, not wf, assert wf, fpf-dom wf, Id wf, id-deq wf, fpf-trivial-subtype-top, msg-spec-loc-decl wf, update-spec-decl wf, l all wf, Knd wf, ecl-kinds wf, isrcv wf, ldst wf, lnk wf, Kind-deq wf, normal-da wf, normal-ds wf, update-spec wf, msg-spec wf, ecl wf, fpf wf, ecl-2-3-compat, R-compat-Rplus2, ecl-machine1 wf, ecl-machine2 wf, ecl-machine3 wf, subtype rel self, decl-state wf, ma-valtype wf, bool wf, ecl-1-2-compat, R-compat wf, nat wf, ecl-1-3-compat, R-consistent wf, Rplus wf, event system wf, l-all-iff, IdLnk wf, msg-spec-links wf, ecl-mng-sends wf, msg-spec-loc-decl-implies, es-decls-iff, es-decls-join-single, es-vartype wf, Id sq, member-remove-repeats, idlnk-deq wf, es-decls wf, es-sends-iff functionality, ecl-tags wf, fpf-join wf, fpf-single wf, iff transitivity, eqtt to assert, assert-deq-member, tagged-list-messages wf, fpf-cap wf, rcv wf, bnot wf, eqff to assert, assert of bnot, not functionality wrt iff, es-state-when wf, subtype rel dep function, top wf, es-val wf, es-isrcv wf, mapfilter wf, es-bact wf, es-valtype wf, es-init wf, es-loc-init, es-E wf, es-loc wf, fpf-sub-join-left2, fpf-sub weakening, deq-member wf, es-kind wf, append wf, map wf, deq wf, es-when wf, fpf-join-cap-sq, bool cases, bool sq, fpf-cap-single1, subtype rel wf, ecl-trans-a wf, filter is nil, pi1 wf, pi2 wf, product-deq wf, update-spec-vars wf, ecl-mng-update wf, es-le-self, fpf-ap wf, es-after wf, es-interval-eq, list accum wf, ifthenelse wf, iff imp equal bool, subtype-fpf-cap-void |
Type, da:k:Knd fp
upd:update-spec(ds;da).